// ==++==
// 
//   Copyright (c) Microsoft Corporation.  All rights reserved.
// 
// ==--==
using System;
using System.Collections.Generic;
using System.Text;
using Microsoft.Pex.Framework;
using System.Collections;
using DySy.Framework;
using Microsoft.Pex.Framework.Settings;
using Microsoft.VisualStudio.TestTools.UnitTesting;

namespace DySy.Tests
{
    [TestClass, PexClass, DySyAnalysis]
    public partial class BasicTests
    {
        [PexMethod]
        public void Empty()
        {
        }

        [PexMethod]
        public void OnePath()
        {
            foo(0);
            foo(1);
            foo(2);
            foo(3);
        }

        void foo(int i)
        {
            if (i > 567)
                Console.WriteLine("hello");
        }

        [PexMethod]
        public void Factorial5()
        {
            fac(5);
        }

        int fac(int n)
        {
            if (n <= 1)
                return 1;
            else
                return n * fac(n - 1);
        }

        [PexMethod]
        public void SquareTest()
        {
            square(1);
            square(2);
        }

        int square(int n)
        {
            return n * n;
        }

        [PexMethod]
        public void FactorialLoops()
        {
            facLoop(1);
            facLoop(2);
            facLoop(3);
            facLoop(4);
            facLoop(5);
        }

        int facLoop(int n)
        {
            int x = 1;
            for (int i = 2; i < n; i++)
                x *= i;
            return x;
        }

        [PexMethod]
        public void FactorialLoop()
        {
            facLoop(10);
        }

        public class ArrayParams
        {
            public Node[] field = new Node[] { new Node() };
            public Node[][] field1 = new Node[][] { new Node[] { new Node() } };

            public void araryParamId(Node[] nodeArray)
            {
            }

            public void araryParam(Node[] nodeArray)
            {
                nodeArray[3] = new Node();
            }

            public void arrayParam1Id(Node[][] nodeArrayArray)
            {
            }

            public void arrayParam1(Node[][] nodeArrayArray)
            {
                nodeArrayArray[0][0] = new Node();
                nodeArrayArray[3] = new Node[] { new Node(), null };
            }
        }

        public class StaticFields
        {
            public static int f1 = 0;
            public static int f2 = 0;

            public void modifyStatics()
            {
                f1 += 10;
                Other.field += 10;
            }
        }

        public class DeepParams
        {
            public void deepParam(Node n)
            {
                for (int i = 1; i <= 10; i++)
                    if (n == null)
                    {
                        Console.WriteLine("Nine or fewer nodes");
                        return;
                    }
                    else
                        n = n.next;

                Console.Out.WriteLine("Ten or more nodes");
            }
        }

        public class Other
        {
            public static int field = 0;
        }

        public class Node
        {
            public Node next;
        }

        [PexMethod]
        public void deepParams()
        {
            Node n = new Node();
            n.next = n;
            new DeepParams().deepParam(n);
        }

        [PexMethod]
        public void modifyStatics()
        {
            new StaticFields().modifyStatics();
        }

        [PexMethod]
        public void nodeArray()
        {
            Node[] nodeArray = new Node[10];
            for (int i = 0; i < 8; i++)
                nodeArray[i] = new Node();
            new ArrayParams().araryParam(nodeArray);
            new ArrayParams().araryParamId(nodeArray);

            Node[][] nodeArrayArray = new Node[10][];
            for (int i = 0; i < 10; i++)
                nodeArrayArray[i] = new Node[10];
            for (int i = 0; i < 8; i++)
                nodeArrayArray[i] = nodeArray;
            new ArrayParams().arrayParam1(nodeArrayArray);
            new ArrayParams().arrayParam1Id(nodeArrayArray);
        }

        public class ReturnValue
        {
            public int linearRelation(int x, int y)
            {
                return 3 * x + 4 * y + 5;
            }

            public int squared(int x)
            {
                return x * x;
            }

            public int conditional(int x, int y)
            {
                if (x < y)
                    return 3 * x + 4 * y + 5;
                else
                    return x * y;
            }
        }

        [PexMethod]
        public void linearRelation()
        {
            new ReturnValue().linearRelation(8, 9);
            new ReturnValue().linearRelation(9, 8);
            new ReturnValue().linearRelation(3, 5);
            new ReturnValue().linearRelation(5, 3);
            new ReturnValue().linearRelation(2, 3);

            new ReturnValue().squared(8);
            new ReturnValue().squared(9);
            new ReturnValue().squared(3);
            new ReturnValue().squared(5);
            new ReturnValue().squared(2);

            new ReturnValue().conditional(5, 6);
            new ReturnValue().conditional(6, 5);
        }

        [PexMethod]
        public void LoopVarTest()
        {
            LoopVar("   ");
            LoopVar("foo");

        }

        public string LoopVar(string s)
        {
            bool allSpaces = true;
            for (int i = PexSymbolicValue.Internal.LoopVar("$i", 0);
                i < s.Length;
                i = PexSymbolicValue.Internal.LoopVar("$i", i + 1))
            {
                if (s[i] != ' ')
                    allSpaces = false;
            }
            if (allSpaces)
                return s;
            else
                return "bar";
        }

        private object returnSome()
        {
            return new object();
        }

        [PexMethod]
        public void SomeTest()
        {
            returnSome();
        }

        [PexMethod]
        public void DisjunctionTest()
        {
            disjunctionTest(true, false);
            disjunctionTest(true, true);
        }

        private int disjunctionTest(bool b, bool c)
        {
            if (c)
            {
            }

            if (b)
                return 1;
            else
                return 0;
        }

        [PexMethod]
        public void IsNullOrEmptyTest()
        {
            clean(null);
            clean("");
        }

        string clean(string str)
        {
            if (str == null || str.Length == 0)
            {
                return str;
            }
            return "foo";
        }

        class Stack
        {
            public int Count;
            public int[] Elements;
            public byte ForFun;

            public Stack()
            {
                this.Elements = new int[10];
            }

            public void Push(int x)
            {
                this.Elements[this.Count++] = x;
                this.ForFun++;
                if (this.ForFun > 0) { }
            }

            public bool IsEmpty
            {
                get { return this.Count == 0; }
            }

            public int Pop()
            {
                if (this.Count > 0)
                    return this.Elements[--this.Count];
                else
                    return 0;
            }
        }

        [PexMethod]
        public void InvariantTest()
        {
            Stack s = new Stack();
            s.Push(5);
            s.Push(6);
            PexAssert.IsTrue(!s.IsEmpty);
            s.Pop();
            s.Pop();
            PexAssert.IsTrue(s.IsEmpty);
        }
    }
}
